COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00005 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source

.cb Notes on Lee Blaine's thesis %2Programs for Structured Proofs%1

	My primary impression is that Blaine hasn't faced the fact
(or is glossing it over) that the style of proof used in the
thesis and by EXCHECK generally is suitable only for relatively
easy theorems.

	A major trouble is that there are no examples in which a new
concept has to be introduced that isn't present in the statement
of the theorem or the previous theorems, e.g. the colors of the
squares in the theorem about not being able to tile a checkerboard
with diagonally opposite squares removed or the pairings of integers
with their inverses ⊗(mod_p) in the proof of Wilson's theorem.
I would like to see some discussion of this issue even if it is
too late to improve EXCHECK or to make more experiments.
Otherwise, the thesis is simply misleading about the progress that
has been made in proof-checking.

	It also seems to me that the content of the set theory course
has been oversimplified in order to fit EXCHECK's limitations.  For
example, there is no mention of metatheorems such as those concerning
the relations of the various systems of set theory or independence
or incompleteness.  While I agree that this is beyond the state
of the present art, and a useful body of material can be taught that
doesn't involve it, it is again misleading to ignore the issue.

	There  are a few specific errors that I have noticed.

47 - The rewrite scheme for finite universal quantifiers should
have ∧ instead of ∨ in the conclusion.

73 - The statement of Russell's theorem in the text is garbled.
I mean the English form not the symbolic form.

	I am prepared to sign, but I would like
some consideration of the above criticisms if there is time.

.nofill

John McCarthy, Computer Science Department